/*
 * $Id: ConsentNode.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright 2004
 *    Distributed Systems Research Group
 *    Department of Software Engineering
 *    Faculty of Mathematics and Physics
 *    Charles University, Prague
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.node;

import java.util.HashMap;
import java.util.LinkedList;
import java.util.TreeSet;
import java.util.ArrayList;
import java.util.TreeMap;
import java.util.Iterator;

import org.objectweb.fractal.bpc.checker.DFSR.BadActivityException;
import org.objectweb.fractal.bpc.checker.DFSR.CheckingException;
import org.objectweb.fractal.bpc.checker.DFSR.NoActivityException;
import org.objectweb.fractal.bpc.checker.DFSR.Options;
import org.objectweb.fractal.bpc.checker.state.*;
import org.objectweb.fractal.bpc.checker.state.TransitionPairs.IntPair;
import org.objectweb.fractal.bpc.checker.utils.AnotatedProtocol;

/**
 * Represents the consent operator.
 */
public class ConsentNode extends TreeNode {

    /**
     * ctor.
     * 
     * @param node1
     *            node representing the first protocol to be combined via
     *            consent operator
     * @param node2
     *            node representing the second protocol to be combined via
     *            consent operator
     * @param events
     *            set of events on which to synchronize
     * @param unboundEvents
     *            set of events on which to synchronize
     * @param repository
     *            reference to action repository
     * @param test
     *            true if testing composition errors, false when visualizing
     */
    public ConsentNode(TreeNode node1, TreeNode node2, TreeSet events,
            TreeSet unboundEvents, ActionRepository repository, boolean test) {
        super("(" + node1.protocol + ")%(" + node2.protocol + ")");

        this.events = events;
        this.unboundEvents = unboundEvents;
        this.repository = repository;
        this.topmost = true;
        this.test = test;

        this.nodes = new TreeNode[2];
        this.nodes[0] = node1;
        this.nodes[1] = node2;

        // setup the topmost atribute for the children
        if (node1 instanceof ConsentNode)
            ((ConsentNode) node1).topmost = false;

        if (node2 instanceof ConsentNode)
            ((ConsentNode) node2).topmost = false;

        this.boundEvents = new TreeSet();
        this.boundAtomicActions = new boolean[2][];
        this.dependecies = new LinkedList[2];
        this.delayed = new HashMap();
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getWeight()
     */
    public long getWeight() {
        if (weight != -1)
            return weight;
        else {
            // this is heuristic - potentially it can be a product of subtrees!
            long w1 = nodes[0].getWeight(), w2 = nodes[1].getWeight();
            return weight = (long) (0.5f * w1 * w2 + 0.25f * ((w1 + w2) / 2));
        }
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getInitial()
     */
    public State getInitial() {
        State[] states = new State[2];
        states[0] = nodes[0].getInitial();
        states[1] = nodes[1].getInitial();

        return new CompositeState(states);
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#isAccepting(org.objectweb.fractal.bpc.checker.state.State)
     */
    public boolean isAccepting(State state) {
        CompositeState cstate = (CompositeState) state;

        return (nodes[0].isAccepting(cstate.states[0])) && (nodes[1].isAccepting(cstate.states[1]));
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getTransitions(org.objectweb.fractal.bpc.checker.state.State)
     */
    public TransitionPairs getTransitions(State state) throws InvalidParameterException, CheckingException {
        CompositeState cstate = (CompositeState) state;
        delayed.clear();

        TransitionPairs transp1 = nodes[0].getTransitions(cstate.states[0]);
        TransitionPairs transp2 = nodes[1].getTransitions(cstate.states[1]);

        TransitionPair[] trans1 = transp1.transitions;
        TransitionPair[] trans2 = transp2.transitions;

        currentdeps = new LinkedList();
        dependecies[0] = transp1.deps;
        dependecies[1] = transp2.deps;

        ArrayList result = new ArrayList();
        TreeMap sync = new TreeMap();
        this.boundAtomicActions[0] = new boolean[trans1.length];
        this.boundAtomicActions[1] = new boolean[trans2.length];

        //we divide the transitions of node1 (states[0]) into two groups
        // - that of not present within the synchro events set and the others
        for (int i = 0; i < trans1.length; ++i) {
            Integer key = new Integer(trans1[i].eventIndex);

            if (key.intValue() < 0) {
                //atomic event
                if (makeAtomicTransition(i, trans1, trans2, cstate, result, 0))
                    boundAtomicActions[0][i] = true;
            }

            else if (events.contains(new Integer(ActionRepository.getPure(trans1[i].eventIndex)))) {
                // the following is not necessary since we have to have the
                // deterministic nodes below this node
                /*
                 * if (sync.containsKey(key))
                 * ((ArrayList)sync.get(key)).add(trans1[i]); else { ArrayList
                 * value = new ArrayList(); value.add(trans1[i]); sync.put(new
                 * Integer(trans1[i].eventIndex), value); }
                 */

                sync.put(new Integer(trans1[i].eventIndex), trans1[i]);
                
                
                for (Iterator it = currentdeps.iterator(); it.hasNext(); ) {
                    IntPair item = (IntPair)it.next();
                    
                    if (item.second == trans1[i].eventIndex)
                        it.remove();
                }
                
                delayed.put(key, null);
            }

            // check for missing binding
            else if (topmost && unboundEvents.contains(new Integer(ActionRepository.getPure(trans1[i].eventIndex)))) {
                boolean isResponse = repository.isResponse(trans1[i].eventIndex);
                if ((Options.badactivity) && (test) && (!isResponse))
                    throw new BadActivityException("missing binding for request '" + repository.getItemString(trans2[i].eventIndex) + "':");
            }

            // else just don't synchronize
            else {
                State[] states = new State[2];
                states[0] = trans1[i].state;
                states[1] = cstate.states[1];

                result.add(new TransitionPair(trans1[i].eventIndex, new CompositeState(states)));
            }
        }

        boundEvents.clear();
        boundEvents.addAll(sync.keySet());

        // now complete the result array
        for (int i = 0; i < trans2.length; ++i) {
            Integer key = new Integer(trans2[i].eventIndex);
            if (key.intValue() < 0) {
                //atomic event
                if (!boundAtomicActions[1][i])
                    if (makeAtomicTransition(i, trans2, trans1, cstate, result, 1))
                        boundEvents.removeAll(repository.getAtomicEvents(repository.getInverseAction(trans2[i].eventIndex)));
            }

            else if (events.contains(new Integer(ActionRepository.getPure(trans2[i].eventIndex)))) {
                Integer invkey = new Integer(repository.getInverseAction(trans2[i].eventIndex));
                if (sync.containsKey(invkey)) {
                    /*
                     * Iterator it = ((ArrayList)sync.get(invkey)).iterator();
                     * 
                     * while(it.hasNext()) { State[] states = new State[2];
                     * states[0] = ((TransitionPair)it.next()).state; states[1] =
                     * trans2[i].state;
                     * 
                     * result.add(new
                     * TransitionPair(repository.getTauAction(trans2[i].eventIndex),
                     * new CompositeState(states))); }
                     * 
                     * boundEvents.remove(invkey);
                     */

                    State[] states = new State[2];
                    states[0] = ((TransitionPair) sync.get(invkey)).state;
                    states[1] = trans2[i].state;

                    result.add(new TransitionPair(repository.getTauAction(trans2[i].eventIndex), new CompositeState(states)));
                    
                    
                    for (Iterator it = currentdeps.iterator(); it.hasNext(); ) {
                        IntPair item = (IntPair)it.next();
                        
                        if (item.second == trans2[i].eventIndex)
                            it.remove();
                    }
                    

                    boundEvents.remove(invkey);
                    delayed.put(key, null);
                }

                else { // Bad activity detected
                    boolean isResponse = repository.isResponse(trans2[i].eventIndex);
                    if ((Options.badactivity) && (test) && (!isResponse) && !boundAtomicActions[1][i] && (!unboundEvents.contains(new Integer(ActionRepository.getPure(trans2[i].eventIndex)))))
                        throw new BadActivityException("bad activity(" + repository.getItemString(trans2[i].eventIndex) + "):");
                    else {

                    }
                }
                
                if (topmost && test && unboundEvents.contains(new Integer(ActionRepository.getPure(trans2[i].eventIndex))) && (!repository.isResponse(trans2[i].eventIndex))) {
                    throw new BadActivityException("missing binding for request '" + repository.getItemString(trans2[i].eventIndex) + "':");
                }
            }
            // test the missing binding
            else if (topmost && unboundEvents.contains(new Integer(ActionRepository.getPure(trans2[i].eventIndex)))) {
                boolean isResponse = repository.isResponse(trans2[i].eventIndex);
                if ((Options.badactivity) && (test) && (!isResponse))
                    throw new BadActivityException("missing binding for request '" + repository.getItemString(trans2[i].eventIndex) + "':");
            }

            // else just don't synchronize
            else {
                State[] states = new State[2];
                states[0] = cstate.states[0];
                states[1] = trans2[i].state;

                result.add(new TransitionPair(trans2[i].eventIndex, new CompositeState(states)));
            }
        }

        Iterator it = boundEvents.iterator();

        while (it.hasNext()) {
            int action = ((Integer) it.next()).intValue();
            if ((Options.badactivity) && (test) && (!repository.isResponse(action)))
                throw new BadActivityException("bad activity (" + repository.getItemString(action) + "):");
        }
        
        // check for possible bad activities (delayed ba)
        for (Iterator it2 = delayed.keySet().iterator(); it2.hasNext() ;) {
            IntPair data = (IntPair)delayed.get(it2.next());
            if (data != null)
                throw new BadActivityException("Bad activity (atomic action " +  repository.getItemString(data.first) + " cannot accept " + repository.getItemString(repository.getInverseAction(data.second)) + "). Trace: ");
        }
        
        // eliminating unbound provided operations
        if (topmost) {
	        for (Iterator it3 = result.iterator(); it3.hasNext(); ) {
	            if (unboundEvents.contains(new Integer(ActionRepository.getPure(((TransitionPair)it3.next()).eventIndex))))
	                it3.remove();
	        }
        }

        TransitionPair[] result1 = new TransitionPair[result.size()];
        Iterator it2 = result.iterator();
        int i = 0;

        while (it2.hasNext())
            result1[i++] = (TransitionPair) it2.next();

        // no activity error (=deadlock) detection
        if (result1.length == 0) {
            if ((Options.noactivity) && (test) && (!this.isAccepting(state))) {
                throw new NoActivityException("no activity:");
            }
        }
        
        if (topmost) {
            for (int j = 0; j < result1.length; ++j) {
                if (result1[j].eventIndex < 0) {	//atomic action
                    for (Iterator itt = currentdeps.iterator(); itt.hasNext(); ) {
                        TransitionPairs.IntPair item = (IntPair) itt.next();
                        if (item.first == result1[j].eventIndex)	// error
                            throw new BadActivityException("Atomic action " + repository.getItemString(item.first) + " raised a bad activity exception. Trace:");
                    }
                    
                }
                
            }
        }

        return new TransitionPairs(result1, currentdeps);
    }

    /**
     * Try to make a transition over an atomic action
     * 
     * @param index
     *            index of the action within the first atomic set
     * @param first
     *            set of transitions of the first component
     * @param second
     *            the set of the transitions of the other component
     * @param result
     *            the list for addding the possible transitions
     * @return true if first[index] can be bound to one or more inverse atomic
     *         actions
     */
    private boolean makeAtomicTransition(int index, TransitionPair[] first,
            TransitionPair[] second, CompositeState starting, ArrayList result,
            int tooglebit) throws BadActivityException {

        LinkedList trans = makeTransition(index, first, second, starting, tooglebit);

        if (trans.size() > 0) {
            result.addAll(trans);
            return true;
        } else
            return false;
    }

    /**
     * Try to make a transitive closure of atomic action to satisfy its
     * requirement
     * 
     * @param index
     *            index of the atomic action within the first set to be
     *            performed
     * @param first
     *            the set of possible transitions of the first component
     * @param second
     *            the set of possible transitions of the second component
     * @return list of possible transitions over this atomic action
     */
    private LinkedList makeTransition(int index, final TransitionPair[] first, final TransitionPair[] second, CompositeState starting, int tooglebit) {
        int atomicactionindex = first[index].eventIndex;
        final AtomicAction aaction = repository.getAtomicEvents(atomicactionindex);
        AtomicAction synchroaction = new AtomicAction();
        LinkedList result = new LinkedList();
        LinkedList nosynchro = new LinkedList();
        boolean bound = false;
        //boolean boundsimple = false;
        AtomicAction newaa = null;

        Iterator it = aaction.iterator();

        while (it.hasNext()) {
            Integer event = (Integer) it.next();

            if (events.contains(new Integer(ActionRepository.getPure(event.intValue()))))
                synchroaction.add(event);
            else
                nosynchro.add(event);
        }

        //check if the atomic action is well formed - i.e. contains only one
        // simple action for this binding
        /*if (synchroaction.size() > 1)
            //not well formed!
           throw new BadActivityException("Atomic action not well-formed (" + repository.getItemString(first[index].eventIndex) + ") - contains more than 1 simple action on a binding. Trace: ");
        */
        // no synchro on this binding
        if (synchroaction.size() == 0) {
            State[] states = new State[2];
            states[tooglebit] = first[index].state;
            states[1 - tooglebit] = starting.states[1 - tooglebit];
            result.add(new TransitionPair(first[index].eventIndex, new CompositeState(states)));
            
            // keep all items with transition within the dependency list
            for (Iterator it2 = dependecies[tooglebit].iterator(); it2.hasNext(); ) {
                TransitionPairs.IntPair item = (TransitionPairs.IntPair)it2.next();
                if (item.first == first[index].eventIndex)
                    currentdeps.add(item);
            }
            return result;
        }

        else {
            
            if (synchroaction.size() == 1) {
        
                int synchroactionidx = ((Integer) synchroaction.first()).intValue();
        
                for (int i = 0; i < second.length; ++i) {
                    if ((tooglebit == 1) && boundAtomicActions[0][i])
                        continue;
        
                    if (second[i].eventIndex >= 0) { //single action - no atomic
                        // action
                        if (synchroactionidx == repository.getInverseAction(second[i].eventIndex)) {
                            //bound
                            newaa = new AtomicAction(aaction);
                            newaa.remove(new Integer(synchroactionidx));
                            newaa.add(new Integer(repository.getTauAction(synchroactionidx)));
                            State[] states = new State[2];
                            states[tooglebit] = first[index].state;
                            states[1 - tooglebit] = second[i].state;
                            result.add(new TransitionPair(repository.getItemIndex(newaa), new CompositeState(states)));
                            
                            /*
                            for (Iterator it2 = dependecies[tooglebit].iterator(); it2.hasNext(); ) {
                                TransitionPairs.IntPair item = (TransitionPairs.IntPair)it2.next();
                                if (item.first == first[index].eventIndex) {
                                    item.first = repository.getItemIndex(newaa);
                                    currentdeps.add(item);
                                }
                            }
        
                            if (repository.isResponse(synchroactionidx))
                                currentdeps.add(new TransitionPairs.IntPair(first[index].eventIndex, synchroactionidx));
                             */
                            
                            boundAtomicActions[1 - tooglebit][i] = true;
                            bound = true;
                            //boundsimple = true;
                        }
        
                        else if (repository.isResponse(synchroactionidx)) {
                            //bad activity may occur here, but cannot find out now,
                            // cache the information
                            currentdeps.add(new TransitionPairs.IntPair(first[index].eventIndex, second[i].eventIndex));
                        }
        
                    } else { // atomic action
                        newaa = new AtomicAction(repository.getAtomicEvents(second[i].eventIndex));
        
                        //Iterator it2 = repository.getAtomicEvents(second[i].eventIndex).iterator();
        
                        //while (it2.hasNext()) {
                        //    Integer event = (Integer) it2.next();
                            
                            
                            //AtomicAction bounding = new AtomicAction(repository.getAtomicEvents(event.intValue()));
                            boolean was = newaa.remove(new Integer(repository.getInverseAction(synchroactionidx)));
        
                            if (was) {
                                //newaa.remove(new Integer(synchroactionidx));
                                newaa.add(new Integer(repository.getTauAction(synchroactionidx)));
                                //newaa.addAll(bounding);
                                State[] states = new State[2];
                                states[tooglebit] = first[index].state;
                                states[1 - tooglebit] = second[i].state;
                                result.add(new TransitionPair(repository.getItemIndex(newaa), new CompositeState(states)));
                                bound = true;
                                boundAtomicActions[1 - tooglebit][i] = true;
                                 
                                /*
                                for (Iterator it3 = dependecies[tooglebit].iterator(); it3.hasNext(); ) {
        	                        TransitionPairs.IntPair item = (TransitionPairs.IntPair)it3.next();
        	                        if (item.first == first[index].eventIndex) {
        	                            item.first = repository.getItemIndex(newaa);
        	                            currentdeps.add(item);
        	                        }
        	                    }
        
                                for (Iterator it3 = dependecies[1-tooglebit].iterator(); it3.hasNext(); ) {
        	                        TransitionPairs.IntPair item = (TransitionPairs.IntPair)it3.next();
        	                        if (item.first == event.intValue()) {
        	                            item.first = repository.getItemIndex(newaa);
        	                            currentdeps.add(item);
        	                        }
        	                    }
        	                    */
        
                                //break;	   			// only one simple action can be bound at this binding 
                            }
                        //}
                    }
                }
    	        
    	        if (!bound) {
    	            if (repository.isResponse(synchroactionidx)) {
    	                for (Iterator iterator = currentdeps.iterator(); iterator.hasNext() ;) {
    	                    TransitionPairs.IntPair item = (TransitionPairs.IntPair)iterator.next();
    	                    
    	                    if (item.first == first[index].eventIndex) { 
    	                        if (repository.isResponse(item.second)) {
    	                            if (!delayed.containsKey(new Integer(item.second)))
    	                                delayed.put(new Integer(item.second), item);
    	                                    
    	                            //throw new BadActivityException("Bad activity (atomic action " +  repository.getItemString(first[index].eventIndex) + " cannot accept " + repository.getItemString(repository.getInverseAction(item.second)) + "). Trace: ");
    	                        } else {
    	                            iterator.remove();
    	                            delayed.put(new Integer(item.second), null);
    	                        }
    	                    }
    	                }
    
    	                return result;
    	            }
    	            else {		// unbound request!
    
    	                for (Iterator it2 = dependecies[tooglebit].iterator(); it2.hasNext(); ) {
                            TransitionPairs.IntPair item = (TransitionPairs.IntPair)it2.next();
                            if (item.first == first[index].eventIndex) {
                                item.first = repository.getItemIndex(newaa);	// that should work
                                currentdeps.add(item);
                            }
                        }
    
    	                result.add(new TransitionPair(first[index].eventIndex, null));
    	                currentdeps.add(new TransitionPairs.IntPair(first[index].eventIndex, synchroactionidx));
    	                return result;
    	            }
    	        }
    	        else
    	            return result;
            }
            
            else { // more than 1 simple event on this binding - strudl...
                TreeSet atomiccandidates = new TreeSet();
                TreeSet newcandidates = new TreeSet();
                
                // select only atomic actions
                for (int i = 0; i < second.length; ++i)
                    if (second[i].eventIndex < 0)
                        atomiccandidates.add(new IntPair(second[i].eventIndex, i));
                
                //iteratate over second atomic actions to determine, which are boundable
                for (it = atomiccandidates.iterator(); it.hasNext(); ) {
                    IntPair pair = (IntPair)it.next();
                    AtomicAction aa = new AtomicAction(repository.getAtomicEvents(pair.first));
                    int secondindex = pair.second;
                    boolean bound2 = false;
                    for (Iterator it2 = synchroaction.iterator(); it2.hasNext(); ) {
                        Integer event = (Integer)it2.next();
                        boolean was = aa.remove(new Integer(repository.getInverseAction(event.intValue())));
                        if (was) {
                            int tauaction = repository.getTauAction(event.intValue());
                            aa.add(new Integer(tauaction));
                            bound2 = true;
                        }
                        // if at least one of the single action is not bound, this atomic action is not added to new candidates 
                        else {
                            bound2 = false;
                            break;
                        }
                    }
                    if (bound2) {
                        newcandidates.add(new IntPair(repository.getItemIndex(aa), secondindex));
                        boundAtomicActions[1 - tooglebit][secondindex] = true;
                    }
                }
                
                boolean containsresponse = false;
                
                if (newcandidates.size() == 0) {
                    for (it = synchroaction.iterator(); it.hasNext(); )
                        if (repository.isResponse(((Integer)it.next()).intValue())) {
                            containsresponse = true;
                            break;
                        }
                    
                                        
                    if (containsresponse) {
                        for (Iterator iterator = currentdeps.iterator(); iterator.hasNext() ;) {
                            TransitionPairs.IntPair item = (TransitionPairs.IntPair)iterator.next();
                            
                            if (item.first == first[index].eventIndex) { 
                                if (repository.isResponse(item.second)) {
                                    if (!delayed.containsKey(new Integer(item.second)))
                                        delayed.put(new Integer(item.second), item);
                                            
                                    //throw new BadActivityException("Bad activity (atomic action " +  repository.getItemString(first[index].eventIndex) + " cannot accept " + repository.getItemString(repository.getInverseAction(item.second)) + "). Trace: ");
                                } else {
                                    iterator.remove();
                                    delayed.put(new Integer(item.second), null);
                                }
                            }
                        }
    
                        return result;
                    }
                    else {      // unbound request!
    
                        for (Iterator it2 = dependecies[tooglebit].iterator(); it2.hasNext(); ) {
                            TransitionPairs.IntPair item = (TransitionPairs.IntPair)it2.next();
                            if (item.first == first[index].eventIndex) {
                                item.first = repository.getItemIndex(newaa);    // that should work
                                currentdeps.add(item);
                            }
                        }
    
                        result.add(new TransitionPair(first[index].eventIndex, null));
                        currentdeps.add(new TransitionPairs.IntPair(first[index].eventIndex, ((Integer)synchroaction.first()).intValue()));
                        return result;
                    }
                    
                    
                }
                else {
                    
                    for (it = newcandidates.iterator(); it.hasNext(); ) {
                        IntPair pair = (IntPair)it.next();
                        State[] states = new State[2];
                        states[0] = first[index].state;
                        states[1] = second[pair.second].state;
                        
                        AtomicAction aa1 = repository.getAtomicEvents(pair.first);
                        AtomicAction aa2 = repository.getAtomicEvents(second[pair.second].eventIndex);
                        
                        for (Iterator it2 = aa2.iterator(); it2.hasNext(); ) {
                            int idx = ((Integer)it2.next()).intValue();
                            if (!((aa1.contains(new Integer(repository.getInverseAction(idx))) || (aa1.contains(new Integer(repository.getTauAction(idx)))))))
                                aa1.add(new Integer(idx));
                        }
                        
                        
                        result.add(new TransitionPair(repository.getItemIndex(aa1), new CompositeState(states)));
                    }
                }
                
                return result;
            }
        }
    }
        
    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getTypeName()
     */
    public String[] getTypeName() {
        String[] result = { "Consent", "%" };
        return result;
    }

    /**
     * 
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#forwardCut(java.util.TreeSet)
     */
    public TreeNode forwardCut(TreeSet livingevents) {
        TreeSet exlivev = new TreeSet(livingevents);

        exlivev.addAll(events);
        TreeSet exlivev2 = new TreeSet(exlivev);

        nodes[0] = nodes[0].forwardCut(exlivev);
        nodes[1] = nodes[1].forwardCut(exlivev2);

        if (nodes[0] == null)
            nodes[0] = new NullNode();

        if (nodes[1] == null)
            nodes[1] = new NullNode();

        return this;
    }

    /**
     * @see org.objectweb.fractal.bpc.checker.node.TreeNode#getAnotatedProtocol(org.objectweb.fractal.bpc.checker.state.State)
     */
    public AnotatedProtocol getAnotatedProtocol(State state) {
        CompositeState cstate = (CompositeState) state;
        int nodecnt = nodes.length;
        String result = new String();
        ArrayList indicesresult = new ArrayList();

        for (int i = 0; i < nodecnt; ++i) {
            AnotatedProtocol subresult = nodes[i].getAnotatedProtocol((cstate != null) ? cstate.states[i] : null);

            for (int j = 0; j < subresult.indices.size(); ++j)
                indicesresult.add(new Integer(((Integer) subresult.indices.get(j)).intValue() + result.length()));

            result += subresult.protocol;

            if (i < nodecnt - 1)
                result += " % ";
        }

        return new AnotatedProtocol(result, indicesresult);
    }

    //--------------------------------------------------------------------------

    /**
     * The set of synchronizing events for the consent operator
     */
    final private TreeSet events;

    /**
     * The set of events on unbound interfaces
     */
    final private TreeSet unboundEvents;

    /**
     * Action repository for seeking the tau and other event indices
     */
    private ActionRepository repository;

    /**
     * Flag for the topmost consent operator. This is necessary for bad activity
     * detection
     */
    private boolean topmost;

    /**
     * Determines whether the tree is intended for testing or visualization
     */
    private boolean test;

    /**
     * Set of already bound events
     */
    private TreeSet boundEvents;

    /**
     * Indices of bound atomic actions within the first sequence
     */
    private boolean[][] boundAtomicActions;
    
    /**
     * Dependencies for atomic actions from subtrees
     */
    private LinkedList[] dependecies;

    /**
     * atomic action dependecies
     */
    private LinkedList currentdeps;
    
    /**
     * Delayed bad activity exceptions
     */
    private HashMap delayed;
}
